\begin{tabbing}
$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $i$:Id, ${\it es}$:ES.
\\[0ex]($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. loc($e$) $=$ $i$ $\Rightarrow$ valtype($e$) $\subseteq\rho$ ${\it da}$(kind($e$))?Top)
\\[0ex]$\Rightarrow$ (\=$\forall$$e_{1}$, $e_{2}$, $e_{3}$:E.\+
\\[0ex]loc($e_{1}$) $=$ $i$
\\[0ex]$\Rightarrow$ $e_{1}$ $\leq$ $e_{2}$ 
\\[0ex]$\Rightarrow$ $e_{1}$ $\leq$ $e_{3}$ 
\\[0ex]$\Rightarrow$ es{-}hist\{i:l\}(${\it es}$;$e_{1}$;$e_{2}$) $=$ es{-}hist\{i:l\}(${\it es}$;$e_{1}$;$e_{3}$) $\in$ event{-}info(${\it ds}$;${\it da}$) List
\\[0ex]$\Rightarrow$ $e_{2}$ $=$ $e_{3}$)
\-
\end{tabbing}